$\forall$$A$, $B$, $C$:Type, $g$:($A$$\rightarrow$($B$ + Top)), $f$:($A$$\rightarrow$$B$$\rightarrow$$C$), $x$:$A$.
\\[0ex]($\uparrow$can{-}apply($f$ o' $g$;$x$)) $\Rightarrow$ (do{-}apply($f$ o' $g$;$x$) $\sim$ ($f$($x$,do{-}apply($g$;$x$))))